The MICRO-PLANNER System (PLNR) is essentially as  described  in  the
original  MICRO-PLANNER REFERENCE MANUAL as available from the MIT AI
Lab (Memo No. 203A).  Portions of this manual, along with a good deal
of explanatory material, are available on-line as LSP:PLNR.MAN, which
is an alternate  reference  manual  produced  by  Bruce  Baumgart  at
Stanford (SAILON No. 67).

When  PLNR  is  started  you are communicating with a top-level READ,
THVAL, PRINT loop.  The "$" macro  character  is  active,  and  since
repeated  shifting  is  tough  on  the  pinky,  ":" may be used as an
alternative to "$".  Thus :←X is equivalent to $←X is  equivalent  to
(THNV X).  To make matters even easier, ::X is equivalent to $?X.

Note  that  THCONSE,  THANTE, and THERASING may be used to define and
assert  theorems,  and  THEDIT  may  be  used  to  edit  them.    The
prettyprinter  prints  theorems correctly, and THSTATE may be used to
dump theorems to a file (by including it as an argument to a DSKOUT).

Finally, note that the  THTRACE  package  as  described  in  the  MIT
documentation provides a powerful trace facility for PLNR.